COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "let.pub[let,jmc]" source
C00004 ENDMK
C⊗;
.require "let.pub[let,jmc]" source;
∂CSL Professor K. Mani Chandy↓Dept. of Computer Sciences
↓University of Texas↓Austin, TX 78712-1188∞

Dear Professor Chandy:

	Sorry for the long delay in the letter about Boyer and Moore.
I was hoping to find a previous letter I thought I had written so
I could update it.

	I think Boyer and Moore have done the best work in automated
theorem proving.  It's best, because almost everyone else has shirked
the problem of generating mathematical inductions.
Moreover, they have applied their methods to a wider variety of
problems than other workers.

	Their productivity seems to have increased since they moved
to the University of Texas, and several students have broken new
ground in using their system for mathematical proofs.  I have in
mind in particular the proof of Gauss's law of quadratic reciprocity.

	Finally, they have published regularly and informtively.  I
believe their work is better described in papers and books than
anyone else's.  Supefinally, their programs have been made available
in Interlisp, Maclisp and Lisp Machine Lisp to anyone who wants them.

	In short I think there is an ideal case for making them full
professors.

.sgn